COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Preliminary description of axiom schemas
C00005 ENDMK
C⊗;
Preliminary description of axiom schemas

	1. There are no special rules, merely an extension of the use
of the rules already given in the writeup.  Likewise and axiom schema
is simply an axiom with predicate parameters in it.

	2. As we know, an axiom is can be used anywhere a step can be
used just by referring to the axiom name.  This use is extended by allowing
where AXNAM would appear, the form AXNAM[PP1←XX1,...,PPn←XXn] where the
PPi are predicate parameters appearing in the axiom, and XXi are 
expressions assigned to these parameters and the assignments are done
successively rather than simultaneously.  (This is hack that won't be
fixed for a long time perhaps not in this edition of FOL).  

	3. An XXi is a well formed formula preceded by λ, any number of
indvars and ..  Thus

	λ x y z.<wff>.

	4. The arity of the predicate parameter must be ≤ the number
of variables following the λ.  The indicated λ-conversion on the first
arity variables is done automatically.  (You can get "not enough λ variables"
as an error message).  The remaining variables are treated as parameters
of the entire expression and are universally generalized on the outside.

	5. The :# mechanism can be used to take pieces out of the resulting
formula.

Examples:
*****DECLARE PREDPAR F 1,INDVAR X;
*****AXIOM INDUCTION: F(0)∧∀X.(F(X)⊃F(X+1)⊃∀X.F(X);
*****DECLARE INDVAR a b;
*****ai INDUCTION[F←λb a.a+b=b+a];

∀a.((a+0)=(0+a)∧∀X.((a+X)=(X+a)⊃(a+(X+1))=((X+1)+a))⊃∀X.(a+X)=(X+a))

*****ai INDUCTION[F←λb.∀a.a+b=b+a];

∀a.(a+0)=(0+a)∧∀X.(∀a.(a+X)=(X+a)⊃∀a.(a+(X+1))=((X+1)+a))⊃∀X a.(a+X)=(X+a)

*****ai INDUCTION[F←λb X.X+b=b+X];

∀X.(X+0)=(0+X)∧∀X1.((X+X1)=(X1+X)⊃(X+(X1+1))=((X1+1)+X))⊃∀X2(X+X2)=(X2+X))